∧i REPL[A←λx t.(∀y.(yεt ≡ yεa ∧ R(x,y)))];
∧i SEP[B←λy.R(x,y)];
∀E ↑ a;
∃E ↑ w;
ASSUME ∀z.(zεt≡(zεa∧R(x,z)));
∀E EXT w,t;
∀E ↑↑↑ z;
∀E ↑↑↑ z;
TAUT zεw≡zεt 7:8;
∀I ↑ z;
TAUT w=t 6,10;
⊃I 5⊃↑;
ASSUME w=t;
SUBST ↑ IN 4;
⊃I ↑↑⊃↑;
TAUT ∀z.(zεt≡(zεa∧R(x,z)))≡w=t 12,15;
∀I ↑ t;
∃I ↑ w←y;
∀I ↑ x;
TAUT 1:#2 1,19;
∀e 20 a;
∃E ↑ v;
∀E UNION v;
∀E ↑ z;
ASSUME zεunion v;
TAUT ∃t.(tεv∧zεt) 24:25;
∃E ↑ t;
∀E 22 t;
TAUT ∃s.(sεa∧∀y.(yεt≡(yεa∧R(s,y)))) 27:28;
∃E ↑ s;
∧E ↑:#2;
∀E ↑ z;
TAUT zεa 27,32;
⊃I 25⊃↑;
ASSUME zεa;
∧I SEP[B←λy.R(z,y)];
∀E ↑ a;
∃E ↑ y;
∧I (35 38);
∃I ↑ z←s;
∀E 22 y;
TAUT yεv 40:41;
∀E 38 z;
∀E EQUIV1 z;
TAUT zεy 35,43:44;
∧I (42 45);
∃I ↑ y←t;
TAUT zεunion v 24,47;
⊃I 35⊃↑;
TAUT zεunion v≡zεa 34,49;
∀I ↑ z;
∀E EXT union v,a;
TAUT union v=a 51:52;
ASSUME rεv;
∀E 22 r;
TAUT ∃s.(sεa∧∀y.(yεr≡(yεa∧R(s,y)))) 54:55;
ASSUME xεr∧yεr;
∃E ↑↑ s;
∧E ↑:#2;
∀E ↑ x;
∀E ↑↑ y;
∀E EQUIV2 s,x;
∀E EQUIV3 x,s,y;
TAUT R(x,y) 57,60:63;
⊃I 57⊃↑;
∀I ↑ x y;
⊃I 54⊃↑;
∀I ↑ r;
assume r1εv∧r2εv;
ASSUME ∃x.(xεr1∧xεr2);
∀E 22 r1;
∀E 22 r2;
TAUT ∃s.(sεa∧∀y.(yεr1≡(yεa∧R(s,y)))) 69,71;
TAUT ∃s.(sεa∧∀y.(yεr2≡(yεa∧R(s,y)))) 69,72;
∃E ↑↑ s;
∃E ↑↑ t;
∧E ↑↑:#2;
∧E ↑↑:#2;
∀E ↑↑ x;
∀E ↑↑ x;
∀E 77 w;
∀E 78 w;
label A;
∃e 70 x;
∀e EQUIV2 s w;
∀E EQUIV2 x,t;
∀E EQUIV2 w t;
∀E EQUIV2 x s;
∀E EQUIV3 w,s,x;
∀E EQUIV3 w,x,t;
∀E EQUIV3 w,t,x;
label B;
∀E EQUIV3 w,x,s;
taut wεr1 ≡ wεr2 A:B 79:82;
∀i ↑ w;
∀e EXT r1 r2;
taut r1=r2 93 94;
⊃i 70 ↑;
⊃i 69 ↑;
taut ↑:#1∧↑:#2#1⊃↑:#2#2 ↑;
∀i ↑ r1 r2;
taut 53:∧68:∧↑: 53 68 ↑;
∃i ↑ v;
∀i ↑ a;